/-
Copyright (c) 2024 Joël Riou. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joël Riou
-/
import Mathlib.Algebra.Category.Grp.Abelian
import Mathlib.Algebra.Category.Grp.Adjunctions
import Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
import Mathlib.CategoryTheory.Sites.Abelian
import Mathlib.CategoryTheory.Sites.ConstantSheaf

/-!
# Sheaf cohomology

Let `C` be a category equipped with a Grothendieck topology `J`.
We define the cohomology types `Sheaf.H F n` of an abelian
sheaf `F` on the site `(C, J)` for all `n : ℕ`. These abelian
groups are defined as the `Ext`-groups from the constant abelian
sheaf with values `ℤ` (actually `ULift ℤ`) to `F`.

We also define `Sheaf.cohomologyPresheaf F n : Cᵒᵖ ⥤ AddCommGrp`
which is the presheaf which sends `U` to the `n`th `Ext`-group
from the free abelian sheaf generated by the presheaf
of sets `yoneda.obj U` to `F`.

## TODO
* if `U` is a terminal object of `C`, define an isomorphism
  `(F.cohomologyPresheaf n).obj (Opposite.op U) ≃+ Sheaf.H F n`.
* if `U : C`, define an isomorphism
  `(F.cohomologyPresheaf n).obj (Opposite.op U) ≃+ Sheaf.H (F.over U) n`.

-/

assert_not_exists TwoSidedIdeal

universe w' w v u

namespace CategoryTheory

open Abelian

variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}

namespace Sheaf

section

variable (F : Sheaf J AddCommGrp.{w})
  [HasSheafify J AddCommGrp.{w}] [HasExt.{w'} (Sheaf J AddCommGrp.{w})]

/-- The cohomology of an abelian sheaf in degree `n`. -/
def H (n : ℕ) : Type w' :=
  Ext ((constantSheaf J AddCommGrp.{w}).obj (AddCommGrp.of (ULift ℤ))) F n

noncomputable instance (n : ℕ) : AddCommGroup (F.H n) := by
  dsimp only [H]
  infer_instance

end

section

variable [HasSheafify J AddCommGrp.{v}] [HasExt.{w'} (Sheaf J AddCommGrp.{v})]

variable (J) in
/-- The bifunctor which sends an abelian sheaf `F` and an object `U` to the
`n`th Ext-group from the free abelian sheaf generated by the
presheaf of sets `yoneda.obj U` to `F`. -/
noncomputable def cohomologyPresheafFunctor (n : ℕ) :
    Sheaf J AddCommGrp.{v} ⥤ Cᵒᵖ ⥤ AddCommGrp.{w'} :=
  Functor.flip
    (Functor.op (yoneda ⋙ (Functor.whiskeringRight _ _ _).obj
      AddCommGrp.free ⋙ presheafToSheaf _ _) ⋙ extFunctor n)

/-- Given an abelian sheaf `F`, this is the presheaf which sends `U`
to the `n`th Ext-group from the free abelian sheaf generated by the
presheaf of sets `yoneda.obj U` to `F`. -/
noncomputable abbrev cohomologyPresheaf (F : Sheaf J AddCommGrp.{v}) (n : ℕ) :
    Cᵒᵖ ⥤ AddCommGrp.{w'} :=
  (cohomologyPresheafFunctor J n).obj F

end

end Sheaf

end CategoryTheory
